(declare-fun w^01 () Int)
(declare-fun e^01 () Int)
(declare-fun y^01 () Int)
(declare-fun Nl23__const_8^01 () Int)
(declare-fun Nl23d^01 () Int)
(declare-fun o^01 () Int)
(declare-fun Nl23sqr11^01 () Int)
(declare-fun w^02 () Int)
(declare-fun e^02 () Int)
(declare-fun y^02 () Int)
(declare-fun Nl23__const_8^02 () Int)
(declare-fun Nl23d^02 () Int)
(declare-fun o^02 () Int)
(declare-fun Nl23sqr11^02 () Int)
(declare-fun f () Int)
(declare-fun p () Int)
(declare-fun lam0n3 () Int)
(declare-fun v () Int)
(declare-fun lam0n6 () Int)
(declare-fun z () Int)
(declare-fun x () Int)
(declare-fun q () Int)
(declare-fun g () Int)
(declare-fun a () Int)
(declare-fun r () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun s () Int)
(declare-fun lam2n7 () Int)
(declare-fun j () Int)
(declare-fun ^ () Int)
(declare-fun ^0 () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun k () Int)
(declare-fun lam5n7 () Int)
(declare-fun t () Int)
(declare-fun l () Int)
(declare-fun d () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun aa () Int)
(declare-fun u () Int)
(declare-fun lam6n8 () Int)
(assert (<= o^01 1 Nl23sqr11^01))
(assert (<= y^02 1))
(assert (<= 0 Nl23__const_8^02 1))
(assert (<= o^02 1))
(assert (or (and (>= lam0n3 0) (>= v 0) (> (+ p lam0n3) 0) (= (+ (+ 1 v) (* w^02 z)) 0 (+ p e^02) 0 (+ (- (- 1) lam0n3 v) (* y^02 z))) (distinct v 0) (= Nl23d^02 0 (+ p (* o^01 lam0n6) (* o^02 z)) 0 (* Nl23sqr11^01 lam0n6))) (and (> x 0) (= (- w^01) a 0 (* Nl23sqr11^02 r) (- Nl23sqr11^01)))))
(assert (or (and (= w^02 0 (mod e^01 lam0n6) 0 (+ (* y^02 z)) 0 Nl23d^01 0 (div 0 g))) (and (>= i 0) (> (* q lam2n7) 0) (= h 2 (* Nl23d^01 s)) (= (- Nl23sqr11^02) 0))))
(assert (and (<= (+ q (* 2 ^0) (* e^02 ^0 2)) 0) (or (and (>= b c k t 0) (> t 0) (= e^02 y^02 (+ (* ^ lam5n7) Nl23__const_8^02) (* ^ lam5n7) 0 l d m)) (and (>= n aa u 0) (>= lam6n8 (* q lam6n8) 0) (= (+ (* w^02 lam6n8) 1) 0 (+ aa (* e^02 lam6n8)) (+ (* y^01 u))) (= (+ (* Nl23__const_8^01 u) (* Nl23__const_8^02 lam6n8)) (+ (* Nl23d^02 lam6n8)) (+ (* o^01 u) (* o^02 lam6n8)) (* ^ lam6n8) 0)) (and (= j (div 0 0) 0) (>= f z 0 (+ v (* Nl23__const_8^02)) 0 z)))))
(check-sat)
